Nuprl Definition : l_contains
11,40
postcript
pdf
A
B
==
a
A
. (
a
B
)
latex
clarification:
l_contains(
T
;
A
;
B
) == l_all(
A
;
T
;
a
.(
a
B
T
))
latex
Definitions
(
x
l
)
,
x
L
.
P
(
x
)
FDL editor aliases
l_contains
origin
B == 
a
A. (a B)
B T)) B == aA. (a B)
B T)) l)xL. P(x)